『［2021CAPE公開セミナー］論理学上級 Ⅱ-2「カリー・ハワード対応と『証明のデータ型としての命題』観」』 - pogi-log

『［2021CAPE公開セミナー］論理学上級 Ⅱ-2「カリー・ハワード対応と『証明のデータ型としての命題』観」』

↑CAPE公開セミナー

『［2021CAPE公開セミナー］論理学上級 Ⅱ-1「ラッセルのパラドックスと3つの対策」』 ←　→ 『［2021CAPE公開セミナー］論理学上級 Ⅱ-3 証明論的意味論としてのマーティン・レーフの構成的型理論』

矢田部俊介. [2021CAPE公開セミナー] 論理学上級 Ⅱ-2「カリー・ハワード対応と『証明のデータ型としての命題』観」 . 2021

https://www.youtube.com/watch?v=q02uYIc0s6g

1972年にPer Martin-Löfが構成的型理論を発表

カリー＝ハワード対応

動的意味論

命題の意味は(正規な)証明によって定まる

Propositions as Types

証明の(データ)型としての命題

証明は帰納的に構成される

証明を関数として解釈する

A→B

矛盾⊥

証明が存在しないため空集合

原始命題の証明

公理そのものを証明とみなす

$ a : A